x, y:. x < y  (x < y) 

latex

Definitions	A, {T}, P  Q, , P  Q, P & Q, P  Q, t  T, Top, tt, if b then t else f fi , r - s, qpositive(r), t.1, r * s, r + s, q_le(r;s), qeq(r;s), t.2, , gset, , x f y, a < b, goset, a <p b, <+>, a < b, r < s, P  Q, x:A. B(x), False
Lemmas	not functionality wrt iff, assert of bnot, assert of eq int, assert of lt int, or functionality wrt iff, assert of bor, and functionality wrt iff, assert of band, assert wf, iff transitivity, not wf, iff functionality wrt iff, isint-int